Maybe better to skip lectures...

1. Basic coursework
2. Go programming
3. Material has not changed compared to last year
4. Last part on session types was optional, it is not anymore.
5. Go will not be in exams, but will be in coursework
6. Slides are text-rich
7. Books: (If individual project, then read the advanced book) • Introductory book: Communicating and Mobile Systems: the π-calculus (Milner 1999) • Advanced books: The π-calculus: a Theory of Mobile Processes (Sangiorgi, Walker 2001)

Pi-calculus

1. The π-calculus evolved from (value-passing) CCS, but it is more expressive

```go func main() {

// Shared buffer with a size a := main(chan int, 1) b := make(chan bool, 1)

go func () { a <- 1; // a with the bar on top (send the integer 1 to channel a) } ()

i := <- a // Input a b <- true // Output b

} ```

Pi-calculus

• (ν a)(a⟨b⟩ | (ν c)c⟨a⟩) =α (ν d)(d⟨b⟩ | (ν c)c⟨d⟩ "=α" means that it is alpha-convertible
• The intuition is that α-conversion preserves each difference between names.
• Substitution:
  • A substitution {a/x} applied to a process P (denoted by P{a/x}), has the effect of replacing all the free occurrences of x in P with a.
  • If the new name clashes with a bound variable, rename the bound variable (and he binding)
• Replication:
  • !P ≡ P | !P
  • The way of expressing infinite computation
• Abstraction of a bound variable:
  • a ̸∈ fn(P) =⇒ P | (ν a)Q ≡ (ν a)(P | Q)

• ν a creates a new channel a
• a(x) passes a variable x to a channel a
• You can output channels (since you know what they are before you output them)
• You cannot receive channels, since you don't know that what you receive will be a channel
• A "new"ed channel is bound everywhere within its scope (even if it is outputted)
• You cannot rename free variables during substitution
• Substitution does not have to preserve the original meaning of the exepression:
  • In fact, it is the means of altering the expression
• The variable becomes bound in continuation process if it is received in the earlier parts of the process

-